T:Type, L1, L2:(T List), a, b, c:T.
no_repeats(T;L2)
 L1  L2
 adjacent(T;L1;b;a)
 adjacent(T;L2;c;a)
 (b before c  L2  (b = c)) 

latex

Definitions	L1  L2, no_repeats(T;l), adjacent(T;L;x;y), x before y  l, left + right, P  Q, x:AB(x), P  Q, x:A. B(x), s = t, t  T, Type, type List
Lemmas	sublist wf, l before wf, adjacent wf, no repeats wf, adjacent-sublist, before-adjacent